(*----------------------------------------------------------------------(C)-*)
(* Copyright (C) 2006 -2012 Konstantin Korovin and The University of Manchester.
   This file is part of iProver - a theorem prover for first - order logic.

   iProver is free software: you can redistribute it and / or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   (at your option) any later version.
   iProver is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
   See the GNU General Public License for more details.
   You should have received a copy of the GNU General Public License
   along with iProver. If not, see < http:// www.gnu.org / licenses />. *)
(*----------------------------------------------------------------------[C]-*)

open Lib
open Logic_interface

module SymSet = Symbol.Set
type sym_set = Symbol.sym_set

type csig = Clause.clause_signature



let get_sym_types sym = Symbol.get_stype_args_val_def sym

module SymbMap = Symbol.Map

let less_map_ref = Parser_types.less_map
let range_map_ref = Parser_types.range_map
let is_ess_less_range symb =
  (Symbol.is_essential_input symb)
    &&
  ((SymbMap.mem symb !less_map_ref) || (SymbMap.mem symb !range_map_ref))

let neg_symb = Symbol.symb_neg
(*let equality_symb = Symbol.symb_equality*)
let typed_equality_symb = Symbol.symb_typed_equality

let v0 = Var.get_first_var Symbol.symb_type_types
let v1 = Var.get_next_var v0
let v2 = Var.get_next_var v1
let v3 = Var.get_next_var v2
let v4 = Var.get_next_var v3

(* creates term from var and adds to term_db*)
(* let term_var var = TermDB.add_ref (Term.create_var_term var) term_db_ref *)

let tv0 = add_var_term v0
let tv1 = add_var_term v1
let tv2 = add_var_term v2
let tv3 = add_var_term v3
let tv4 = add_var_term v4

let term_var_typed vtype vval =
  add_var_term (Var.create vtype vval)


(*
  let add_fun_term symb args =
  TermDB.add_ref (Term.create_fun_term symb args) term_db_ref
 *)

(*
  let equality_term t s =
  let args = [t; s] in
  add_fun_term equality_symb args
 *)


(*
  let typed_equality_term stype_term t s =
  let args = [stype_term; t; s] in
  add_fun_term typed_equality_symb args

  let typed_equality_term_sym eq_type_sym t s =
  let eq_type = (add_fun_term eq_type_sym []) in
  typed_equality_term eq_type t s

  let neg_atom atom =
  let args = [atom] in
  add_fun_term neg_symb args

(*
  let dis_equality t s =
  neg_atom (equality_term t s)
 *)

  let dis_typed_equality stype t s =
  neg_atom (typed_equality_term stype t s)
 *)

(*
  let assign_eq_ax_param ax =
  Clause.assign_is_eq_axiom true ax;
(*	Clause.set_bool_param true Clause.input_under_eq ax;*) (* not used now*)
  (* Clause.assign_axiom_history Clause.Eq_Axiom ax *)
  Clause.assign_tstp_source_axiom_equality ax
 *)


let create_eq_ax_clause ax_lits =
  let tstp_source = Clause.tstp_source_axiom_equality in 
  let ax_clause = create_clause tstp_source ax_lits in
  Clause.assign_is_eq_axiom true ax_clause;
  ax_clause

(*
  let reflexivity_axiom () =
  let reflex_term = equality_term tv0 tv0 in
  let refl_ax = Clause.create [reflex_term] in
  assign_eq_ax_param refl_ax;
  refl_ax

(* axiom x0=x1 & x2 = x1 => x2=x0 is equiv to trans & symmetry *)
  let trans_symmetry_axiom () =
  let x01 = dis_equality tv0 tv1 in
  let x21 = dis_equality tv2 tv1 in
  let x20 = equality_term tv2 tv0 in
  let trans_sim_ax = Clause.create [x01; x21; x20] in
  assign_eq_ax_param trans_sim_ax;
  trans_sim_ax
 *)

(*-----typed versions--------*)
(* universal axioms over all types *)
(* we can preinstantiate for types occuring in the problem *)

(*-------reflexifity-------*)
let typed_reflexivity_axiom_var context =
  let reflex_term = add_typed_equality_term tv0 tv1 tv1 in
  let refl_ax = create_eq_ax_clause [reflex_term] in
  refl_ax

(* some times it is useful to have instantiatied eq axioms *)
let typed_reflexivity_axiom_type eq_type_sym =
  let eq_type = (add_fun_term eq_type_sym []) in
  let ttv0 = term_var_typed eq_type_sym 0 in
  let reflex_term = add_typed_equality_term eq_type ttv0 ttv0 in
  let refl_ax = create_eq_ax_clause [reflex_term] in
  refl_ax

let typed_reflexivity_axiom_type_set eq_type_set =
  let f eq_type rest =
    (typed_reflexivity_axiom_type eq_type):: rest
  in
  SymSet.fold f eq_type_set []

(*---------trans_symmetry---------*)

let typed_trans_symmetry_axiom_var () =
  (* tv3 is used for types *)
  (*  let type_var_term = tv3 in *)
  let x01 = add_typed_disequality_term tv0 tv1 tv2 in
  let x21 = add_typed_disequality_term tv0 tv3 tv2 in
  let x20 = add_typed_equality_term tv0 tv3 tv1 in
  let trans_sim_ax = create_eq_ax_clause [x01; x21; x20] in
  trans_sim_ax

let typed_trans_symmetry_axiom_type eq_type_sym =
  let eq_type = (add_fun_term eq_type_sym []) in
  (* tv3 is used for types *)
  (*  let type_var_term = tv3 in *)
  let ttv0 = term_var_typed eq_type_sym 0 in
  let ttv1 = term_var_typed eq_type_sym 1 in
  let ttv2 = term_var_typed eq_type_sym 2 in
  
  let x01 = add_typed_disequality_term eq_type ttv0 ttv1 in
  let x21 = add_typed_disequality_term eq_type ttv2 ttv1 in
  let x20 = add_typed_equality_term eq_type ttv2 ttv0 in
  let trans_sim_ax = create_eq_ax_clause [x01; x21; x20] in
  trans_sim_ax

let typed_trans_symmetry_axiom_type_set eq_type_set =
  let f eq_type rest =
    (typed_trans_symmetry_axiom_type eq_type):: rest
  in
  SymSet.fold f eq_type_set []

(*-------symmetry----------*)
(* used in finite_models *)
let typed_symmetry_axiom_sym eq_type_sym =
  let eq_type = (add_fun_term eq_type_sym []) in
  let ttv0 = term_var_typed eq_type_sym 0 in
  let ttv1 = term_var_typed eq_type_sym 1 in
  let neg_eq_x0_x1 = add_typed_disequality_term eq_type ttv0 ttv1 in
  let eq_x1_x0 = add_typed_equality_term eq_type ttv1 ttv0 in
  let sym_ax = create_eq_ax_clause [neg_eq_x0_x1; eq_x1_x0] in
  sym_ax

(*--------------typed version--------------*)
(* congruence axioms: given a hash table of types *)
(*(types with which sorted_euqality occurs)       *)
(* and a function f(x_1,..,x_n) we add congrunce axiom w.r.t. to the types table *)

module SymbTbl = Hashtbl.Make (Symbol)

let typed_congruence_axiom eq_type_set symb =
  match (Symbol.get_stype_args_val symb) with
  | Def (type_args, type_value) ->
      if type_args = []
      then
	(None)
      else				
	let fresh_vars_env = Var.init_fresh_vars_env () in
	let rec get_args_dis_lits
	    current_type_args args1 args2 dis_eq_lits =
	  (match current_type_args with
	  | h:: tl ->
	      (*     out_str ("h: "^(Symbol.to_string h)^"\n");*)
	      if (SymSet.mem h eq_type_set)
	      then
		begin
		  let fresh_var1 = Var.get_next_fresh_var fresh_vars_env h in
		  let fresh_var2 = Var.get_next_fresh_var fresh_vars_env h in
		  let fresh_var_term1 = (add_var_term fresh_var1) in
		  let fresh_var_term2 = (add_var_term fresh_var2) in
		  
		  get_args_dis_lits										
		    tl
		    (fresh_var_term1:: args1)
		    (fresh_var_term2:: args2)
		    ((add_typed_disequality_term
			(add_fun_term h [])
			fresh_var_term1
			fresh_var_term2):: dis_eq_lits)
		end
	      else
		(* same varaibles *)
		begin
		  let fresh_var = Var.get_next_fresh_var fresh_vars_env h in
		  let fresh_var_term = (add_var_term fresh_var) in
		  get_args_dis_lits
		    tl
		    (fresh_var_term:: args1)
		    (fresh_var_term:: args2)
		    dis_eq_lits
		end
	  |[] ->
	      ((List.rev args1), (List.rev args2), (List.rev dis_eq_lits))
	  )
	in
	let (args1, args2, dis_eq_lits) =
	  get_args_dis_lits
	    type_args [] [] [] in
	if (dis_eq_lits = [])
	then
	  (None)
	else
	  if (Symbol.is_pred symb)
	  then
	    let pred = add_fun_term symb args1 in
	    let neg_pred = add_neg_atom (add_fun_term symb args2) in
	    let pred_congr_ax = create_eq_ax_clause  (pred:: neg_pred:: dis_eq_lits)
	    in
	    Some(pred_congr_ax)
	  else
	    (let pos_part =
	      let t = add_fun_term symb args1 in
	      let s = add_fun_term symb args2 in
	      add_typed_equality_term (add_fun_term type_value []) t s
	    in
	    let fun_congr_ax = create_eq_ax_clause (pos_part:: dis_eq_lits) in
	    Some(fun_congr_ax)
	    )
  | Undef ->
      (None)

(* typed_congr_axiom_list_sym_set *)
(* generic function for getting congruence based on csig.eq_type_set             *)
(* internaly the function uses a closure of eq_type_set *)
(* under function application    *)
(*(e.g. a in eq_type_set then val_type of f(..,a,..) is also in eq_type_set *)

(* it also closes signature under function application ! *)
let typed_congr_axiom_list csig =
  (* we close eq_type_set first *)
  (*  let closed_eq_type_set = ref csig.Clause.sig_eq_types in*)
  let rec f symb =
    if (SymSet.mem symb csig.Clause.sig_eq_types)
    then ()
    else
      begin
	let (arg_types, val_type) = get_sym_types symb in
	List.iter f arg_types;
	let arg_is_in_closed_eq_type_set =
	  (List.exists
	     (fun arg_sym -> (SymSet.mem arg_sym csig.Clause.sig_eq_types))
	     arg_types
	  )
	in
	if (arg_is_in_closed_eq_type_set) && (not (val_type == Symbol.symb_bool_type))
	then
	  (csig.Clause.sig_eq_types <- SymSet.add val_type csig.Clause.sig_eq_types
	  )
	else ()
      end
  in
  SymSet.iter f csig.Clause.sig_fun_preds;
  
  (*  let uf_eq_types = UF_ST.create 301 in *)
  
  let f symb rest =
    match (typed_congruence_axiom csig.Clause.sig_eq_types symb) with
    | Some ax ->
	(* out_str ("ax: "^(Clause.to_string ax)^"\n --------------\n");*)
	ax:: rest
    | None -> rest
  in
  SymSet.fold f csig.Clause.sig_fun_preds []

let typed_eq_axioms_sig csig =
  let typed_cong_ax_list = typed_congr_axiom_list csig in
  if (SymSet.is_empty csig.Clause.sig_eq_types)
  then
    []
  else
    (
     let typed_reflexivity_ax =
       typed_reflexivity_axiom_type_set csig.Clause.sig_eq_types in
     
     let typed_trans_symmetry_ax =
       typed_trans_symmetry_axiom_type_set csig.Clause.sig_eq_types in
     
     let eq_axioms =
       ((typed_reflexivity_ax)@((typed_trans_symmetry_ax)@typed_cong_ax_list)) in
     eq_axioms
    )

(*module UF_ST = Union_find.Make(Symbol)*)

(* it should be closed under funct application later *)
(* returns (sym_set, eq_types_set) *)

let get_symb_and_type_eq_set_basic clause_list =
  let csig = Clause.clause_list_signature clause_list in
  csig

let eq_axiom_list clause_list =
  (*  out_str_debug (SymbolDB.to_string !symbol_db_ref);*)
  let csig = get_symb_and_type_eq_set_basic clause_list in
  typed_eq_axioms_sig csig

(*--------------------------------------------*)
let distinct_ax_list () =
  let default_type_term = (add_fun_term Symbol.symb_default_type []) in
  if (Symbol.is_essential_input Symbol.symb_typed_equality)
  then
    (
     let dist_axioms_one_term term term_list =
       let f rest cterm =
	 let dis_eq_term = (add_typed_disequality_term default_type_term term cterm) in
	 let tstp_source = Clause.tstp_source_axiom_distinct in
	 let dis_ax = create_clause tstp_source [dis_eq_term] in
	 (* Clause.assign_axiom_history Clause.Distinct_Axiom dis_ax; *)					
	 dis_ax:: rest
       in
       List.fold_left f [] term_list
     in
     let rec distinct_axioms_from_one_dist' rest_axs cur_term dist_terms_rest =
       let new_axs = (dist_axioms_one_term cur_term dist_terms_rest)@rest_axs in
       match dist_terms_rest with
       | h:: tl -> distinct_axioms_from_one_dist' new_axs h tl
       |[] -> new_axs
     in
     let distinct_axioms_from_one_dist rest_axs dist_term_list =
       match dist_term_list with
       | h:: tl -> distinct_axioms_from_one_dist' rest_axs h tl
       |[] -> rest_axs
     in
     List.fold_left distinct_axioms_from_one_dist [] !Parser_types.distinct
    )
  else
    []

(*------------ less range axioms -------------------------------*)
(* we do not need congruence axioms for less_i and range_i_j    *)

let bit_index_str i =
  "$$bitIndex"^(string_of_int i)

let stype_bit_index = (Symbol.create_stype [] Symbol.symb_ver_bit_index_type)

let bit_index_type_term () =
  add_fun_term Symbol.symb_ver_bit_index_type []

let bit_index_var vval = 
  Var.create Symbol.symb_ver_bit_index_type vval

let bit_index_var_term vval = 
  add_var_term (bit_index_var vval)


let bit_index_symb i =
  let symb =
    (Symbol.create_from_str_type (bit_index_str i) stype_bit_index)
  in
  SymbolDB.add_ref symb symbol_db_ref

let bit_index_term i =
  add_fun_term (bit_index_symb i) []

let bit_index_atom symb i =
  add_fun_term symb [(bit_index_term i)]

let get_max_bit_index () =
  let f_less symb i curr_max =
    if ((curr_max < i) && (Symbol.is_essential_input symb))
    then
      ((*out_str ("Symbol "^(Symbol.to_string symb)^" "^(string_of_int i)^"\n"); *)
	i)
    else
      curr_max
  in
  (* less does not include the ind_bound: +1 *)
  let max_less = (SymbMap.fold f_less !less_map_ref 0) - 1 in
  (* out_str ("\n max_less: "^(string_of_int max_less)^"\n");*)
  (* we assume bit-vector notation: biggest first (71,0) *)
  let f_range symb (i, j) curr_max =
    if ((curr_max < i) && (Symbol.is_essential_input symb))
    then
      i
    else
      curr_max
  in
  let max_less_range = SymbMap.fold f_range !range_map_ref max_less in
  (* out_str ("\n max_less_range: "^(string_of_int max_less_range)^"\n");*)
  max_less_range

(*
  let always_true_ax symb =
  Clause.create [(add_fun_term symb [tv0])]

  let always_false_ax symb =
  Clause.create [(neg_atom (add_fun_term symb [tv0]))]
 *)


(*----------------*)
let less_pos_axs symb max_pos_ind =
  let f rest i =
    (create_clause Clause.tstp_source_axiom_less [(bit_index_atom symb i)]):: rest in
  fold_down_interval f 0 (max_pos_ind -1) []

let less_neg_axs symb max_pos_ind max_ind =
  let f rest i =
    (create_clause Clause.tstp_source_axiom_less
       [(add_neg_atom (bit_index_atom symb i))]):: rest in
  fold_down_interval f max_pos_ind max_ind []

let less_eq_ax symb max_pos_ind =
  let bv0 = bit_index_var_term 0 in
  let f rest i =
    (add_typed_equality_term (bit_index_type_term ()) (bit_index_term i) bv0):: rest in
  let eq_terms = fold_down_interval f 0 (max_pos_ind -1) [] in
  let neg_less_term = add_neg_atom (add_fun_term symb [bv0]) in
  create_clause Clause.tstp_source_axiom_less (neg_less_term:: eq_terms)

(*-------------*)

let range_pos_axs symb min_int_ind max_int_ind =
  let f rest i =
    (create_clause Clause.tstp_source_axiom_range [(bit_index_atom symb i)]):: rest in
  fold_down_interval f min_int_ind max_int_ind []

let range_neg_axs symb min_int_ind max_int_ind max_ind =
  let f rest i =
    (create_clause Clause.tstp_source_axiom_range [(add_neg_atom (bit_index_atom symb i))]):: rest in
  let left = fold_down_interval f 0 (min_int_ind -1) [] in
  let right = fold_down_interval f (max_int_ind +1) max_ind [] in
  left@right

let range_eq_ax symb min_int_ind max_int_ind =
  let bv0 = bit_index_var_term 0 in
  let f rest i =
    (add_typed_equality_term (bit_index_type_term ()) (bit_index_term i) bv0):: rest in
  let eq_terms = fold_down_interval f min_int_ind max_int_ind [] in
  let neg_range_term = add_neg_atom (add_fun_term symb [bv0]) in
  create_clause Clause.tstp_source_axiom_range (neg_range_term:: eq_terms)

(*let range_axiom_via_less range_symb *)
(* less axioms should be added after the range axioms since mode less symbols can be added *)

(*
  let range_axiom_via_less range_symb
 *)

let less_axioms' max_ind =
  let f symb i rest =
    (* consider to uncomment later *)
    (* if (i = 0)
       then
       (always_false_ax symb):: rest
       else
       if (i = max_ind +1)
       then
       (always_true_ax symb):: rest
       else
     *)
    if (Symbol.is_essential_input symb)
    then
      (
       let symb_axs =
	 (less_eq_ax symb i):: ((less_pos_axs symb i)
				@(less_neg_axs symb i max_ind)) in
       symb_axs@rest
      )
    else
      rest
  in
  SymbMap.fold f !less_map_ref []

let less_axioms () =
  let max_ind = get_max_bit_index () in
  let less_axioms = less_axioms' max_ind in
  (* Clause.assign_axiom_history_cl_list Clause.Less_Axiom less_axioms; *)
  less_axioms

let range_axioms' max_ind =
  let f symb (max_int_ind, min_int_ind) rest =
    (* if uncommented then incorrect sat result on  *)
    (*Examples/attachments_2011_06_09_from_FMCAD2010_built_in_less_range/bpbimodalm_B2ConcreateClk_no_range_ax.cnf*)
    (*
      if (min_int_ind =0 && max_int_ind = max_ind)
      then
      (always_true_ax symb):: rest
      else
     *)
    if (Symbol.is_essential_input symb)
    then
      (
       ((range_eq_ax symb min_int_ind max_int_ind)::
	((range_pos_axs symb min_int_ind max_int_ind)
	   (*@(range_neg_axs symb min_int_ind max_int_ind max_ind)*)))@rest
      )
    else
      rest
  in
  SymbMap.fold f !range_map_ref []

let range_axioms () =
  let max_ind = get_max_bit_index () in
  let range_axioms = range_axioms' max_ind in
  (* Clause.assign_axiom_history_cl_list Clause.Less_Axiom range_axioms; *)
  range_axioms

let less_range_axioms () =
  (* out_str "\n\n out less map\n\n";
     SymbMap.iter (fun symb _ -> out_str (Symbol.to_string symb)) !less_map_ref;
     out_str "\n\n end out less map\n\n";
   *)
  let max_ind = get_max_bit_index () in
  
  (* out_str
     (Clause.clause_list_to_tptp (less_axioms' max_ind)); *)
  
  let less_range_axioms =
    (less_axioms' max_ind) @ (range_axioms' max_ind)
  in		
  less_range_axioms

(*--------------- Brand's transformation -------------------*)
(*--------------- Flattening -> no congrunce axioms --------*)

(* move *)
module TermHashKey =
  struct
    type t = term
    let equal = (==)
    let hash = Term.get_fast_key
  end


(* will have several uses*)

module TermHash = Hashtbl.Make(TermHashKey)

(*
(* move *)
  let rec get_max_var_term current_max_var_ref term =
  match term with
  | Term.Fun (_, args, _) ->
  Term.arg_iter (get_max_var_term current_max_var_ref) args
  | Term.Var (v, _) ->
  if (Var.compare v !current_max_var_ref) > 0
  then
  (current_max_var_ref := v)
  else ()

  let get_max_var clause =
  let var_ref = ref (Var.get_first_var ()) in
  Clause.iter (get_max_var_term var_ref) clause;
  !var_ref
 *)

(*---------Basic flattening------------------------*)
(* Flattening of a clause is done in two stages:                      *)
(* First, we build a hash table (var_env) mapping non-var term into bvars. *)
(* Second, we use var_env  to build flat terms.            *)
(* In "term_flattening_env var_env max_var_ref term"       *)
(* max_var is max var used                                 *)
(* the input term itself also added to the the var_env     *)
(* if a function term t statisfies add_term_to_def_test    *)
(* we do not need to go                                    *)
(* to subterms  but add 1. a definition t->x into env and  *)
(* 2. a definition into term_def_table (def. of all subterms of t are also added) *)
(* and later add  \neg R_t(x) to the clause *)

let b_orig  = 0 
let b_fresh = 1 (* bound for making vars fresh *)

let rec term_flattening_env renaming_env var_env term =
  match term with
  | Term.Var _ -> ()
  | Term.Fun (symb, args, _) ->
      if (TermHash.mem var_env term)
      then ()
      else
	(
	 (
	  (*
	    if (Symbol.is_fun symb)
	    && (add_term_to_def_test term)
	    then
	    ((* out_str ("Adding to add_term_def_table term: "
		^(Term.to_string term)^"\n");*)
	    add_term_def_table term)
	    else
	   *)
	  (Term.arg_iter (term_flattening_env renaming_env var_env) args)
	 );
	 (* if (Symbol.is_fun symb)
	    then
	  *)
	 (
	  let t_type = Symbol.get_val_type_def symb in 						
	  let ren_var = SubstBound.find_renaming renaming_env (b_fresh, (SubstBound.get_next_unused_var renaming_env t_type)) in
	  let ren_var_term = add_var_term ren_var in 
	  TermHash.add var_env term ren_var_term					
	 )
	   (*	 else ()*)
	)

let flat_term_to_var renaming_env var_env t =
  match t with 
  | Term.Var(v,_) -> 
      let t_type = Var.get_type v in 						
      let ren_var = SubstBound.find_renaming renaming_env (b_orig, (SubstBound.get_next_unused_var renaming_env t_type)) in
      add_var_term ren_var
  | Term.Fun (_,_,_) ->
      (			try
	(*     term_flattening_env var_env max_var_ref t;*)
	TermHash.find var_env t
      with Not_found -> failwith "flat_term_to_var: Not_found"
	 )
	
let flat_top renaming_env var_env term =
  match term with
  | Term.Fun (symb, args, _) ->
      Term.arg_iter (term_flattening_env renaming_env var_env) args;
      let new_args =
	Term.arg_map (fun t -> flat_term_to_var renaming_env var_env t) args in
      TermDB.add_ref (Term.create_fun_term_args symb new_args) term_db_ref
  | Term.Var _ -> term

let flat_lit_env renaming_env var_env lit =
  let f atom =
    match atom with
    | Term.Fun (symb, args, _) ->
	if (symb == Symbol.symb_typed_equality)
	then
	  match (Term.arg_to_list args) with
	  | [eq_type; t1; t2] ->
	      let new_t1 = flat_top renaming_env var_env t1 in
	      let new_t2 = flat_top renaming_env var_env t2 in
	      add_typed_equality_term eq_type new_t1 new_t2
	  | _ -> failwith "flat_lit_env 1"
		
	else
	  flat_top renaming_env var_env atom
    | Term.Var _ -> failwith "flat_lit_env 2"
  in
  TermDB.add_ref (Term.apply_to_atom f lit) term_db_ref

(*---------------------------------*)
let flat_clause clause =
  let renaming_env = SubstBound.init_renaming_env () in
  let var_env = TermHash.create 19 in
  let lit_list = Clause.get_literals clause in
  let flat_lits_without_neg_def =
    List.map (flat_lit_env renaming_env var_env) lit_list in
  (*let default_type_term = (add_fun_term Symbol.symb_default_type []) in*)
  let dis_eq_term t s =
    let t_type = Term.get_term_type t in 
    let t_type_term = (add_fun_term t_type []) in
    (add_typed_disequality_term t_type_term t s) 
  in
  let f t x rest =
    (dis_eq_term (flat_top renaming_env var_env t) x):: rest in
  let neg_def = TermHash.fold f var_env [] in
  create_clause (Clause.tstp_source_flattening clause) (neg_def@flat_lits_without_neg_def)

let eq_axioms_flatting clause_list =
  if (Symbol.is_essential_input Symbol.symb_typed_equality)
  then
    (			
	let flat_clauses = List.map flat_clause clause_list in
	let eq_ax = [(typed_reflexivity_axiom_var ()); (typed_trans_symmetry_axiom_var ())] in
	eq_ax@flat_clauses
       )
  else
    clause_list

(*----------------Commented Below---------------------*)

(*
(*---------------------*)
(* returns ([v_1;..;v_n],[v'_1;...;v'_n]) to be used in congruence axioms*)
  let rec get_two_vlists current_var n =
  if n = 0 then ([],[])
  else
  let next_var = Var.get_next_var current_var in
  let new_current_var = Var.get_next_var next_var in
  let (rest1, rest2) = get_two_vlists new_current_var (n -1) in
  ((term_var current_var):: rest1, (term_var next_var):: rest2)

  exception Arity_non_positive
  let congr_axiom symb =
  let arity = Symbol.get_arity symb in
  if arity <= 0 then raise Arity_non_positive
  else
  (let (vlist1, vlist2) = get_two_vlists v0 arity in
  let var_dis_part =
  List.rev_map2 dis_equality vlist1 vlist2
  in
  match (Symbol.get_type symb)
  with
  | Symbol.Fun ->
  let pos_part =
  let t = add_fun_term symb vlist1 in
  let s = add_fun_term symb vlist2 in
  equality_term t s
  in
  let fun_congr_ax =
  Clause.normalise term_db_ref
  (Clause.create (pos_part:: var_dis_part)) in
  assign_eq_ax_param fun_congr_ax;
  fun_congr_ax
  | Symbol.Pred ->
  let pred = add_fun_term symb vlist1 in
  let neg_pred = neg_atom (add_fun_term symb vlist2) in
  let pred_congr_ax =
  Clause.normalise term_db_ref
  (Clause.create (pred:: neg_pred:: var_dis_part))
  in
  assign_eq_ax_param pred_congr_ax;
  pred_congr_ax
  | _ -> failwith "eq_axioms: no congr_axiom for this type of symb "
  )

  let congr_axiom_list () =
  let f symb rest =
  if ((Symbol.is_input symb) & (not (symb == Symbol.symb_equality)))
  then
  match (Symbol.get_type symb) with
  | Symbol.Fun | Symbol.Pred ->
  if (Symbol.get_arity symb) >0
  then
  (congr_axiom symb):: rest
  else rest
  | _ -> rest
  else rest
  in
  SymbolDB.fold f !symbol_db_ref []

  let axiom_list () =
(*  out_str_debug (SymbolDB.to_string !symbol_db_ref);*)
  if (Symbol.is_input equality_symb)
  then
  let cong_ax_list = congr_axiom_list () in
  (reflexivity_axiom ()):: (trans_symmetry_axiom ()):: cong_ax_list
  else []

 *)
(*
  let sym_set = ref SymSet.empty in
  let eq_type_set = ref SymSet.empty in
  let rec get_type_eq_set_form_term t =
  match t with
  | Term.Fun(symb, args, _) ->
  let relevant_args =
  if (symb == Symbol.symb_typed_equality)
  then
  (
  let (eq_type, t1, t2) =
  get_triple_from_list (Term.arg_to_list args) in
  let eq_type_sym = Term.get_top_symb eq_type in
  eq_type_set:= SymSet.add eq_type_sym !eq_type_set;
  Term.list_to_arg [t1; t2]
  )
  else
  (sym_set := SymSet.add symb !sym_set;
  args
  )
  in
  Term.arg_iter get_type_eq_set_form_term relevant_args
  | Term.Var _ -> ()
  in
  let get_type_eq_set_form_lit lit =
  get_type_eq_set_form_term (Term.get_atom lit)
  in
  let get_type_eq_set_form_cl cl = Clause.iter get_type_eq_set_form_lit cl in
  List.iter get_type_eq_set_form_cl clause_list;
  (!sym_set,!eq_type_set)
 *)

(*

  let get_type_eq_term t =
  match t with
  | Term.Fun(symb, args, _) ->
  if (symb == Symbol.symb_typed_equality)
  then
  (
  match (Term.arg_to_list args) with
  | stype_term:: _ ->
  (match stype_term with
  | Term.Fun(stype_symb, args, _) -> Some stype_symb
  | _ -> failwith
  ("get_type_eq_term shouldn't happen" ^ Term.to_string t)
  )
  | _ -> failwith
  ("get_type_eq_term shouldn't happen\n" ^ Term.to_string t)
  )
  else
  None
  | _ -> None
 *)

(*
  let typed_congr_axiom_list () =
  let eq_type_table = SymbTbl.create 101 in

  let collect_essential_stypes = function

(* Symbol is a theory symbol (not a type symbol) that occurs in an
   input term *)
  | symb when
  (Symbol.is_essential_input symb) &&
  not (symb == Symbol.symb_typed_equality) ->

  (

(* Get type of arguments and type of result of symbol *)
  match Symbol.get_stype_args_val symb with

(* Type of arguments and result determined *)
  | Def (a, v) ->

(* Add all types to table of types except bool type $o *)
  List.iter
  (function

(* Do not generate axioms for bool type $o *)
  | s when (s == Symbol.symb_bool_type) -> ()

(* Generate axioms for all other types *)
  | s ->

(* Symbol not in table? *)
  if not (SymbTbl.mem eq_type_table s) then

(* Add symbol to table of types *)
  SymbTbl.add eq_type_table s s

  )
  (v :: a)

(* Skip if type is not known *)
  | Undef -> ()

  )

(* Symbol is declared only, but does not occur *)
  | _ -> ()

  in

(* Iterate symbol table to find types to generate axioms for *)
  SymbolDB.iter collect_essential_stypes !symbol_db_ref;

  out_str ("Types to generate congruence axioms for:\n");
  SymbTbl.iter
  (fun s _ -> out_str (Symbol.to_string s))
  eq_type_table;
 *)

(* It is not enough to consider the types in equations only, must
   take the types of all symbols in the input as above *)
(*
(* for $equality_sorted(type, t,s) add type to symb_table *)
  let add_eq_type t =

  match (get_type_eq_term t) with
  | Some symb ->
  if (Symbol.is_essential_input symb)
  then
  (SymbTbl.add eq_type_table symb symb)
  else ()
  | None -> ()
  in
  TermDB.iter add_eq_type !term_db_ref;

  let f symb rest =
  out_str ("eq_ax: "
  ^(Symbol.to_string symb)
  ^" is_essential_input: "
  ^(string_of_bool (Symbol.is_essential_input symb))
  ^" Symbol.is_signature_symb: "
  ^(string_of_bool (Symbol.is_signature_symb symb))^"\n");
  if
  (
  (Symbol.is_essential_input symb)
  &&
  (not (symb == Symbol.symb_typed_equality))
  &&
  (Symbol.is_signature_symb symb)
(* &&
(* We don't need congruence axioms for less and range symbols !*)
(* but slower that with the axioms... *)
   (not (is_less_range symb)) *)
  )
  then
  (
  match (typed_congruence_axiom eq_type_table symb) with
  | Some ax ->
  out_str ("ax: "^(Clause.to_string ax)^"\n --------------\n");
  ax:: rest
  | None -> rest
  )
  else rest
  in
  SymbolDB.fold f !symbol_db_ref []

(*
  out_str "\n----------------get_type_eq_term-------\n";
  out_str ((Symbol.to_string symb)^"\n");
 *)

 *)

(*
  let axiom_list () =
(*  out_str_debug (SymbolDB.to_string !symbol_db_ref);*)
  if (Symbol.is_essential_input Symbol.symb_typed_equality)
  then
  (
  let typed_cong_ax_list = typed_congr_axiom_list () in
  (typed_reflexivity_axiom ()):: (typed_trans_symmetry_axiom ()):: typed_cong_ax_list)
  else []
 *)
